Nuprl Lemma : map-concat
11,40
postcript
pdf
f
:(Top
Top),
L
:(Top List List). map(
f
;concat(
L
)) ~ concat(map(
l
.map(
f
;
l
);
L
))
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
map(
f
;
as
)
,
concat(
ll
)
,
reduce(
f
;
k
;
as
)
,
Y
,
Top
Lemmas
top
wf
,
concat-cons
,
map
wf
,
map
append
sq
origin
f:(Top
Top), L:(Top List List). map(f;concat(L)) ~ concat(map(
l.map(f;l);L)) f:(TopTop), L:(Top List List). map(f;concat(L)) ~ concat(map(l.map(f;l);L)) x:A. B(x)
T